#include <string.h>
#include <sys_call.h>

void printf(const char *fmt, ...)
{
	char buf[100];
	u32_t *argv = (u32_t *)(&fmt) + 1;
	vsprintf(buf, fmt, argv);
	sys_write_tty(buf);
}
